Inference at * 1 
Iof proof for Lemma inconsistent-bool-eq2:



1. ff = tt
  False 

latex

 by (Unfolds ``btrue bfalse bool`` ( -1)) 
CollapseTHEN ((ApFunToHypEquands `Z' case Z
Cof inl(x) => 0
Co| inr(x) => 1  (-1)) 
CollapseTHEN (Auto)) 

latex

C1: 

C1: 1. (inr  ) = (inl  )
C1: 2. case inr   of inl(x) => 0 | inr(x) => 1 = case inl   of inl(x) => 0 | inr(x) => 1
C1:   False
C.

Definitions	case b of inl(x) => s(x) | inr(y) => t(y), #$n, , , ff, tt, left + right, Unit, False, Void
Lemmas	unit wf